Left Termination of the query pattern slowsort_in_2(g, a) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

slowsort(X, Y) :- ','(perm(X, Y), sorted(Y)).
sorted([]).
sorted(.(X, [])).
sorted(.(X, .(Y, Z))) :- ','(le(X, Y), sorted(.(Y, Z))).
perm([], []).
perm(.(X, .(Y, [])), .(U, .(V, []))) :- ','(delete(U, .(X, Y), Z), perm(Z, V)).
delete(X, .(X, Y), Y).
delete(X, .(Y, Z), W) :- delete(X, Z, W).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(X)).
le(0, 0).

Queries:

slowsort(g,a).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

slowsort_in(X, Y) → U1(X, Y, perm_in(X, Y))
perm_in(.(X, .(Y, [])), .(U, .(V, []))) → U5(X, Y, U, V, delete_in(U, .(X, Y), Z))
delete_in(X, .(Y, Z), W) → U7(X, Y, Z, W, delete_in(X, Z, W))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, Y, Z, W, delete_out(X, Z, W)) → delete_out(X, .(Y, Z), W)
U5(X, Y, U, V, delete_out(U, .(X, Y), Z)) → U6(X, Y, U, V, perm_in(Z, V))
perm_in([], []) → perm_out([], [])
U6(X, Y, U, V, perm_out(Z, V)) → perm_out(.(X, .(Y, [])), .(U, .(V, [])))
U1(X, Y, perm_out(X, Y)) → U2(X, Y, sorted_in(Y))
sorted_in(.(X, .(Y, Z))) → U3(X, Y, Z, le_in(X, Y))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(X)) → le_out(0, s(X))
le_in(s(X), s(Y)) → U8(X, Y, le_in(X, Y))
U8(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U3(X, Y, Z, le_out(X, Y)) → U4(X, Y, Z, sorted_in(.(Y, Z)))
sorted_in(.(X, [])) → sorted_out(.(X, []))
sorted_in([]) → sorted_out([])
U4(X, Y, Z, sorted_out(.(Y, Z))) → sorted_out(.(X, .(Y, Z)))
U2(X, Y, sorted_out(Y)) → slowsort_out(X, Y)

The argument filtering Pi contains the following mapping:
slowsort_in(x1, x2)  =  slowsort_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U5(x1, x2, x3, x4, x5)  =  U5(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U7(x1, x2, x3, x4, x5)  =  U7(x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U6(x1, x2, x3, x4, x5)  =  U6(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2, x3)  =  U2(x2, x3)
sorted_in(x1)  =  sorted_in(x1)
U3(x1, x2, x3, x4)  =  U3(x2, x3, x4)
le_in(x1, x2)  =  le_in(x1, x2)
0  =  0
le_out(x1, x2)  =  le_out
s(x1)  =  s(x1)
U8(x1, x2, x3)  =  U8(x3)
U4(x1, x2, x3, x4)  =  U4(x4)
sorted_out(x1)  =  sorted_out
slowsort_out(x1, x2)  =  slowsort_out(x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

slowsort_in(X, Y) → U1(X, Y, perm_in(X, Y))
perm_in(.(X, .(Y, [])), .(U, .(V, []))) → U5(X, Y, U, V, delete_in(U, .(X, Y), Z))
delete_in(X, .(Y, Z), W) → U7(X, Y, Z, W, delete_in(X, Z, W))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, Y, Z, W, delete_out(X, Z, W)) → delete_out(X, .(Y, Z), W)
U5(X, Y, U, V, delete_out(U, .(X, Y), Z)) → U6(X, Y, U, V, perm_in(Z, V))
perm_in([], []) → perm_out([], [])
U6(X, Y, U, V, perm_out(Z, V)) → perm_out(.(X, .(Y, [])), .(U, .(V, [])))
U1(X, Y, perm_out(X, Y)) → U2(X, Y, sorted_in(Y))
sorted_in(.(X, .(Y, Z))) → U3(X, Y, Z, le_in(X, Y))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(X)) → le_out(0, s(X))
le_in(s(X), s(Y)) → U8(X, Y, le_in(X, Y))
U8(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U3(X, Y, Z, le_out(X, Y)) → U4(X, Y, Z, sorted_in(.(Y, Z)))
sorted_in(.(X, [])) → sorted_out(.(X, []))
sorted_in([]) → sorted_out([])
U4(X, Y, Z, sorted_out(.(Y, Z))) → sorted_out(.(X, .(Y, Z)))
U2(X, Y, sorted_out(Y)) → slowsort_out(X, Y)

The argument filtering Pi contains the following mapping:
slowsort_in(x1, x2)  =  slowsort_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U5(x1, x2, x3, x4, x5)  =  U5(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U7(x1, x2, x3, x4, x5)  =  U7(x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U6(x1, x2, x3, x4, x5)  =  U6(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2, x3)  =  U2(x2, x3)
sorted_in(x1)  =  sorted_in(x1)
U3(x1, x2, x3, x4)  =  U3(x2, x3, x4)
le_in(x1, x2)  =  le_in(x1, x2)
0  =  0
le_out(x1, x2)  =  le_out
s(x1)  =  s(x1)
U8(x1, x2, x3)  =  U8(x3)
U4(x1, x2, x3, x4)  =  U4(x4)
sorted_out(x1)  =  sorted_out
slowsort_out(x1, x2)  =  slowsort_out(x2)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

SLOWSORT_IN(X, Y) → U11(X, Y, perm_in(X, Y))
SLOWSORT_IN(X, Y) → PERM_IN(X, Y)
PERM_IN(.(X, .(Y, [])), .(U, .(V, []))) → U51(X, Y, U, V, delete_in(U, .(X, Y), Z))
PERM_IN(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN(U, .(X, Y), Z)
DELETE_IN(X, .(Y, Z), W) → U71(X, Y, Z, W, delete_in(X, Z, W))
DELETE_IN(X, .(Y, Z), W) → DELETE_IN(X, Z, W)
U51(X, Y, U, V, delete_out(U, .(X, Y), Z)) → U61(X, Y, U, V, perm_in(Z, V))
U51(X, Y, U, V, delete_out(U, .(X, Y), Z)) → PERM_IN(Z, V)
U11(X, Y, perm_out(X, Y)) → U21(X, Y, sorted_in(Y))
U11(X, Y, perm_out(X, Y)) → SORTED_IN(Y)
SORTED_IN(.(X, .(Y, Z))) → U31(X, Y, Z, le_in(X, Y))
SORTED_IN(.(X, .(Y, Z))) → LE_IN(X, Y)
LE_IN(s(X), s(Y)) → U81(X, Y, le_in(X, Y))
LE_IN(s(X), s(Y)) → LE_IN(X, Y)
U31(X, Y, Z, le_out(X, Y)) → U41(X, Y, Z, sorted_in(.(Y, Z)))
U31(X, Y, Z, le_out(X, Y)) → SORTED_IN(.(Y, Z))

The TRS R consists of the following rules:

slowsort_in(X, Y) → U1(X, Y, perm_in(X, Y))
perm_in(.(X, .(Y, [])), .(U, .(V, []))) → U5(X, Y, U, V, delete_in(U, .(X, Y), Z))
delete_in(X, .(Y, Z), W) → U7(X, Y, Z, W, delete_in(X, Z, W))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, Y, Z, W, delete_out(X, Z, W)) → delete_out(X, .(Y, Z), W)
U5(X, Y, U, V, delete_out(U, .(X, Y), Z)) → U6(X, Y, U, V, perm_in(Z, V))
perm_in([], []) → perm_out([], [])
U6(X, Y, U, V, perm_out(Z, V)) → perm_out(.(X, .(Y, [])), .(U, .(V, [])))
U1(X, Y, perm_out(X, Y)) → U2(X, Y, sorted_in(Y))
sorted_in(.(X, .(Y, Z))) → U3(X, Y, Z, le_in(X, Y))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(X)) → le_out(0, s(X))
le_in(s(X), s(Y)) → U8(X, Y, le_in(X, Y))
U8(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U3(X, Y, Z, le_out(X, Y)) → U4(X, Y, Z, sorted_in(.(Y, Z)))
sorted_in(.(X, [])) → sorted_out(.(X, []))
sorted_in([]) → sorted_out([])
U4(X, Y, Z, sorted_out(.(Y, Z))) → sorted_out(.(X, .(Y, Z)))
U2(X, Y, sorted_out(Y)) → slowsort_out(X, Y)

The argument filtering Pi contains the following mapping:
slowsort_in(x1, x2)  =  slowsort_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U5(x1, x2, x3, x4, x5)  =  U5(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U7(x1, x2, x3, x4, x5)  =  U7(x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U6(x1, x2, x3, x4, x5)  =  U6(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2, x3)  =  U2(x2, x3)
sorted_in(x1)  =  sorted_in(x1)
U3(x1, x2, x3, x4)  =  U3(x2, x3, x4)
le_in(x1, x2)  =  le_in(x1, x2)
0  =  0
le_out(x1, x2)  =  le_out
s(x1)  =  s(x1)
U8(x1, x2, x3)  =  U8(x3)
U4(x1, x2, x3, x4)  =  U4(x4)
sorted_out(x1)  =  sorted_out
slowsort_out(x1, x2)  =  slowsort_out(x2)
DELETE_IN(x1, x2, x3)  =  DELETE_IN(x2)
SORTED_IN(x1)  =  SORTED_IN(x1)
U41(x1, x2, x3, x4)  =  U41(x4)
U81(x1, x2, x3)  =  U81(x3)
SLOWSORT_IN(x1, x2)  =  SLOWSORT_IN(x1)
PERM_IN(x1, x2)  =  PERM_IN(x1)
U61(x1, x2, x3, x4, x5)  =  U61(x3, x5)
LE_IN(x1, x2)  =  LE_IN(x1, x2)
U11(x1, x2, x3)  =  U11(x3)
U51(x1, x2, x3, x4, x5)  =  U51(x5)
U31(x1, x2, x3, x4)  =  U31(x2, x3, x4)
U71(x1, x2, x3, x4, x5)  =  U71(x5)
U21(x1, x2, x3)  =  U21(x2, x3)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

SLOWSORT_IN(X, Y) → U11(X, Y, perm_in(X, Y))
SLOWSORT_IN(X, Y) → PERM_IN(X, Y)
PERM_IN(.(X, .(Y, [])), .(U, .(V, []))) → U51(X, Y, U, V, delete_in(U, .(X, Y), Z))
PERM_IN(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN(U, .(X, Y), Z)
DELETE_IN(X, .(Y, Z), W) → U71(X, Y, Z, W, delete_in(X, Z, W))
DELETE_IN(X, .(Y, Z), W) → DELETE_IN(X, Z, W)
U51(X, Y, U, V, delete_out(U, .(X, Y), Z)) → U61(X, Y, U, V, perm_in(Z, V))
U51(X, Y, U, V, delete_out(U, .(X, Y), Z)) → PERM_IN(Z, V)
U11(X, Y, perm_out(X, Y)) → U21(X, Y, sorted_in(Y))
U11(X, Y, perm_out(X, Y)) → SORTED_IN(Y)
SORTED_IN(.(X, .(Y, Z))) → U31(X, Y, Z, le_in(X, Y))
SORTED_IN(.(X, .(Y, Z))) → LE_IN(X, Y)
LE_IN(s(X), s(Y)) → U81(X, Y, le_in(X, Y))
LE_IN(s(X), s(Y)) → LE_IN(X, Y)
U31(X, Y, Z, le_out(X, Y)) → U41(X, Y, Z, sorted_in(.(Y, Z)))
U31(X, Y, Z, le_out(X, Y)) → SORTED_IN(.(Y, Z))

The TRS R consists of the following rules:

slowsort_in(X, Y) → U1(X, Y, perm_in(X, Y))
perm_in(.(X, .(Y, [])), .(U, .(V, []))) → U5(X, Y, U, V, delete_in(U, .(X, Y), Z))
delete_in(X, .(Y, Z), W) → U7(X, Y, Z, W, delete_in(X, Z, W))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, Y, Z, W, delete_out(X, Z, W)) → delete_out(X, .(Y, Z), W)
U5(X, Y, U, V, delete_out(U, .(X, Y), Z)) → U6(X, Y, U, V, perm_in(Z, V))
perm_in([], []) → perm_out([], [])
U6(X, Y, U, V, perm_out(Z, V)) → perm_out(.(X, .(Y, [])), .(U, .(V, [])))
U1(X, Y, perm_out(X, Y)) → U2(X, Y, sorted_in(Y))
sorted_in(.(X, .(Y, Z))) → U3(X, Y, Z, le_in(X, Y))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(X)) → le_out(0, s(X))
le_in(s(X), s(Y)) → U8(X, Y, le_in(X, Y))
U8(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U3(X, Y, Z, le_out(X, Y)) → U4(X, Y, Z, sorted_in(.(Y, Z)))
sorted_in(.(X, [])) → sorted_out(.(X, []))
sorted_in([]) → sorted_out([])
U4(X, Y, Z, sorted_out(.(Y, Z))) → sorted_out(.(X, .(Y, Z)))
U2(X, Y, sorted_out(Y)) → slowsort_out(X, Y)

The argument filtering Pi contains the following mapping:
slowsort_in(x1, x2)  =  slowsort_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U5(x1, x2, x3, x4, x5)  =  U5(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U7(x1, x2, x3, x4, x5)  =  U7(x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U6(x1, x2, x3, x4, x5)  =  U6(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2, x3)  =  U2(x2, x3)
sorted_in(x1)  =  sorted_in(x1)
U3(x1, x2, x3, x4)  =  U3(x2, x3, x4)
le_in(x1, x2)  =  le_in(x1, x2)
0  =  0
le_out(x1, x2)  =  le_out
s(x1)  =  s(x1)
U8(x1, x2, x3)  =  U8(x3)
U4(x1, x2, x3, x4)  =  U4(x4)
sorted_out(x1)  =  sorted_out
slowsort_out(x1, x2)  =  slowsort_out(x2)
DELETE_IN(x1, x2, x3)  =  DELETE_IN(x2)
SORTED_IN(x1)  =  SORTED_IN(x1)
U41(x1, x2, x3, x4)  =  U41(x4)
U81(x1, x2, x3)  =  U81(x3)
SLOWSORT_IN(x1, x2)  =  SLOWSORT_IN(x1)
PERM_IN(x1, x2)  =  PERM_IN(x1)
U61(x1, x2, x3, x4, x5)  =  U61(x3, x5)
LE_IN(x1, x2)  =  LE_IN(x1, x2)
U11(x1, x2, x3)  =  U11(x3)
U51(x1, x2, x3, x4, x5)  =  U51(x5)
U31(x1, x2, x3, x4)  =  U31(x2, x3, x4)
U71(x1, x2, x3, x4, x5)  =  U71(x5)
U21(x1, x2, x3)  =  U21(x2, x3)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 4 SCCs with 10 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LE_IN(s(X), s(Y)) → LE_IN(X, Y)

The TRS R consists of the following rules:

slowsort_in(X, Y) → U1(X, Y, perm_in(X, Y))
perm_in(.(X, .(Y, [])), .(U, .(V, []))) → U5(X, Y, U, V, delete_in(U, .(X, Y), Z))
delete_in(X, .(Y, Z), W) → U7(X, Y, Z, W, delete_in(X, Z, W))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, Y, Z, W, delete_out(X, Z, W)) → delete_out(X, .(Y, Z), W)
U5(X, Y, U, V, delete_out(U, .(X, Y), Z)) → U6(X, Y, U, V, perm_in(Z, V))
perm_in([], []) → perm_out([], [])
U6(X, Y, U, V, perm_out(Z, V)) → perm_out(.(X, .(Y, [])), .(U, .(V, [])))
U1(X, Y, perm_out(X, Y)) → U2(X, Y, sorted_in(Y))
sorted_in(.(X, .(Y, Z))) → U3(X, Y, Z, le_in(X, Y))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(X)) → le_out(0, s(X))
le_in(s(X), s(Y)) → U8(X, Y, le_in(X, Y))
U8(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U3(X, Y, Z, le_out(X, Y)) → U4(X, Y, Z, sorted_in(.(Y, Z)))
sorted_in(.(X, [])) → sorted_out(.(X, []))
sorted_in([]) → sorted_out([])
U4(X, Y, Z, sorted_out(.(Y, Z))) → sorted_out(.(X, .(Y, Z)))
U2(X, Y, sorted_out(Y)) → slowsort_out(X, Y)

The argument filtering Pi contains the following mapping:
slowsort_in(x1, x2)  =  slowsort_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U5(x1, x2, x3, x4, x5)  =  U5(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U7(x1, x2, x3, x4, x5)  =  U7(x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U6(x1, x2, x3, x4, x5)  =  U6(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2, x3)  =  U2(x2, x3)
sorted_in(x1)  =  sorted_in(x1)
U3(x1, x2, x3, x4)  =  U3(x2, x3, x4)
le_in(x1, x2)  =  le_in(x1, x2)
0  =  0
le_out(x1, x2)  =  le_out
s(x1)  =  s(x1)
U8(x1, x2, x3)  =  U8(x3)
U4(x1, x2, x3, x4)  =  U4(x4)
sorted_out(x1)  =  sorted_out
slowsort_out(x1, x2)  =  slowsort_out(x2)
LE_IN(x1, x2)  =  LE_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LE_IN(s(X), s(Y)) → LE_IN(X, Y)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

LE_IN(s(X), s(Y)) → LE_IN(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SORTED_IN(.(X, .(Y, Z))) → U31(X, Y, Z, le_in(X, Y))
U31(X, Y, Z, le_out(X, Y)) → SORTED_IN(.(Y, Z))

The TRS R consists of the following rules:

slowsort_in(X, Y) → U1(X, Y, perm_in(X, Y))
perm_in(.(X, .(Y, [])), .(U, .(V, []))) → U5(X, Y, U, V, delete_in(U, .(X, Y), Z))
delete_in(X, .(Y, Z), W) → U7(X, Y, Z, W, delete_in(X, Z, W))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, Y, Z, W, delete_out(X, Z, W)) → delete_out(X, .(Y, Z), W)
U5(X, Y, U, V, delete_out(U, .(X, Y), Z)) → U6(X, Y, U, V, perm_in(Z, V))
perm_in([], []) → perm_out([], [])
U6(X, Y, U, V, perm_out(Z, V)) → perm_out(.(X, .(Y, [])), .(U, .(V, [])))
U1(X, Y, perm_out(X, Y)) → U2(X, Y, sorted_in(Y))
sorted_in(.(X, .(Y, Z))) → U3(X, Y, Z, le_in(X, Y))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(X)) → le_out(0, s(X))
le_in(s(X), s(Y)) → U8(X, Y, le_in(X, Y))
U8(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U3(X, Y, Z, le_out(X, Y)) → U4(X, Y, Z, sorted_in(.(Y, Z)))
sorted_in(.(X, [])) → sorted_out(.(X, []))
sorted_in([]) → sorted_out([])
U4(X, Y, Z, sorted_out(.(Y, Z))) → sorted_out(.(X, .(Y, Z)))
U2(X, Y, sorted_out(Y)) → slowsort_out(X, Y)

The argument filtering Pi contains the following mapping:
slowsort_in(x1, x2)  =  slowsort_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U5(x1, x2, x3, x4, x5)  =  U5(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U7(x1, x2, x3, x4, x5)  =  U7(x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U6(x1, x2, x3, x4, x5)  =  U6(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2, x3)  =  U2(x2, x3)
sorted_in(x1)  =  sorted_in(x1)
U3(x1, x2, x3, x4)  =  U3(x2, x3, x4)
le_in(x1, x2)  =  le_in(x1, x2)
0  =  0
le_out(x1, x2)  =  le_out
s(x1)  =  s(x1)
U8(x1, x2, x3)  =  U8(x3)
U4(x1, x2, x3, x4)  =  U4(x4)
sorted_out(x1)  =  sorted_out
slowsort_out(x1, x2)  =  slowsort_out(x2)
SORTED_IN(x1)  =  SORTED_IN(x1)
U31(x1, x2, x3, x4)  =  U31(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SORTED_IN(.(X, .(Y, Z))) → U31(X, Y, Z, le_in(X, Y))
U31(X, Y, Z, le_out(X, Y)) → SORTED_IN(.(Y, Z))

The TRS R consists of the following rules:

le_in(0, 0) → le_out(0, 0)
le_in(0, s(X)) → le_out(0, s(X))
le_in(s(X), s(Y)) → U8(X, Y, le_in(X, Y))
U8(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
le_in(x1, x2)  =  le_in(x1, x2)
0  =  0
le_out(x1, x2)  =  le_out
s(x1)  =  s(x1)
U8(x1, x2, x3)  =  U8(x3)
SORTED_IN(x1)  =  SORTED_IN(x1)
U31(x1, x2, x3, x4)  =  U31(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ UsableRulesReductionPairsProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

SORTED_IN(.(X, .(Y, Z))) → U31(Y, Z, le_in(X, Y))
U31(Y, Z, le_out) → SORTED_IN(.(Y, Z))

The TRS R consists of the following rules:

le_in(0, 0) → le_out
le_in(0, s(X)) → le_out
le_in(s(X), s(Y)) → U8(le_in(X, Y))
U8(le_out) → le_out

The set Q consists of the following terms:

le_in(x0, x1)
U8(x0)

We have to consider all (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

SORTED_IN(.(X, .(Y, Z))) → U31(Y, Z, le_in(X, Y))
U31(Y, Z, le_out) → SORTED_IN(.(Y, Z))
The following rules are removed from R:

le_in(0, 0) → le_out
le_in(0, s(X)) → le_out
le_in(s(X), s(Y)) → U8(le_in(X, Y))
U8(le_out) → le_out
Used ordering: POLO with Polynomial interpretation [25]:

POL(.(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(0) = 2   
POL(SORTED_IN(x1)) = 1 + x1   
POL(U31(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + x3   
POL(U8(x1)) = 1 + x1   
POL(le_in(x1, x2)) = 2 + x1 + 2·x2   
POL(le_out) = 2   
POL(s(x1)) = 1 + x1   



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ UsableRulesReductionPairsProof
                          ↳ QDP
                            ↳ PisEmptyProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

le_in(x0, x1)
U8(x0)

We have to consider all (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

DELETE_IN(X, .(Y, Z), W) → DELETE_IN(X, Z, W)

The TRS R consists of the following rules:

slowsort_in(X, Y) → U1(X, Y, perm_in(X, Y))
perm_in(.(X, .(Y, [])), .(U, .(V, []))) → U5(X, Y, U, V, delete_in(U, .(X, Y), Z))
delete_in(X, .(Y, Z), W) → U7(X, Y, Z, W, delete_in(X, Z, W))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, Y, Z, W, delete_out(X, Z, W)) → delete_out(X, .(Y, Z), W)
U5(X, Y, U, V, delete_out(U, .(X, Y), Z)) → U6(X, Y, U, V, perm_in(Z, V))
perm_in([], []) → perm_out([], [])
U6(X, Y, U, V, perm_out(Z, V)) → perm_out(.(X, .(Y, [])), .(U, .(V, [])))
U1(X, Y, perm_out(X, Y)) → U2(X, Y, sorted_in(Y))
sorted_in(.(X, .(Y, Z))) → U3(X, Y, Z, le_in(X, Y))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(X)) → le_out(0, s(X))
le_in(s(X), s(Y)) → U8(X, Y, le_in(X, Y))
U8(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U3(X, Y, Z, le_out(X, Y)) → U4(X, Y, Z, sorted_in(.(Y, Z)))
sorted_in(.(X, [])) → sorted_out(.(X, []))
sorted_in([]) → sorted_out([])
U4(X, Y, Z, sorted_out(.(Y, Z))) → sorted_out(.(X, .(Y, Z)))
U2(X, Y, sorted_out(Y)) → slowsort_out(X, Y)

The argument filtering Pi contains the following mapping:
slowsort_in(x1, x2)  =  slowsort_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U5(x1, x2, x3, x4, x5)  =  U5(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U7(x1, x2, x3, x4, x5)  =  U7(x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U6(x1, x2, x3, x4, x5)  =  U6(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2, x3)  =  U2(x2, x3)
sorted_in(x1)  =  sorted_in(x1)
U3(x1, x2, x3, x4)  =  U3(x2, x3, x4)
le_in(x1, x2)  =  le_in(x1, x2)
0  =  0
le_out(x1, x2)  =  le_out
s(x1)  =  s(x1)
U8(x1, x2, x3)  =  U8(x3)
U4(x1, x2, x3, x4)  =  U4(x4)
sorted_out(x1)  =  sorted_out
slowsort_out(x1, x2)  =  slowsort_out(x2)
DELETE_IN(x1, x2, x3)  =  DELETE_IN(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

DELETE_IN(X, .(Y, Z), W) → DELETE_IN(X, Z, W)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
DELETE_IN(x1, x2, x3)  =  DELETE_IN(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

DELETE_IN(.(Y, Z)) → DELETE_IN(Z)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

PERM_IN(.(X, .(Y, [])), .(U, .(V, []))) → U51(X, Y, U, V, delete_in(U, .(X, Y), Z))
U51(X, Y, U, V, delete_out(U, .(X, Y), Z)) → PERM_IN(Z, V)

The TRS R consists of the following rules:

slowsort_in(X, Y) → U1(X, Y, perm_in(X, Y))
perm_in(.(X, .(Y, [])), .(U, .(V, []))) → U5(X, Y, U, V, delete_in(U, .(X, Y), Z))
delete_in(X, .(Y, Z), W) → U7(X, Y, Z, W, delete_in(X, Z, W))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, Y, Z, W, delete_out(X, Z, W)) → delete_out(X, .(Y, Z), W)
U5(X, Y, U, V, delete_out(U, .(X, Y), Z)) → U6(X, Y, U, V, perm_in(Z, V))
perm_in([], []) → perm_out([], [])
U6(X, Y, U, V, perm_out(Z, V)) → perm_out(.(X, .(Y, [])), .(U, .(V, [])))
U1(X, Y, perm_out(X, Y)) → U2(X, Y, sorted_in(Y))
sorted_in(.(X, .(Y, Z))) → U3(X, Y, Z, le_in(X, Y))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(X)) → le_out(0, s(X))
le_in(s(X), s(Y)) → U8(X, Y, le_in(X, Y))
U8(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U3(X, Y, Z, le_out(X, Y)) → U4(X, Y, Z, sorted_in(.(Y, Z)))
sorted_in(.(X, [])) → sorted_out(.(X, []))
sorted_in([]) → sorted_out([])
U4(X, Y, Z, sorted_out(.(Y, Z))) → sorted_out(.(X, .(Y, Z)))
U2(X, Y, sorted_out(Y)) → slowsort_out(X, Y)

The argument filtering Pi contains the following mapping:
slowsort_in(x1, x2)  =  slowsort_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U5(x1, x2, x3, x4, x5)  =  U5(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U7(x1, x2, x3, x4, x5)  =  U7(x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U6(x1, x2, x3, x4, x5)  =  U6(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2, x3)  =  U2(x2, x3)
sorted_in(x1)  =  sorted_in(x1)
U3(x1, x2, x3, x4)  =  U3(x2, x3, x4)
le_in(x1, x2)  =  le_in(x1, x2)
0  =  0
le_out(x1, x2)  =  le_out
s(x1)  =  s(x1)
U8(x1, x2, x3)  =  U8(x3)
U4(x1, x2, x3, x4)  =  U4(x4)
sorted_out(x1)  =  sorted_out
slowsort_out(x1, x2)  =  slowsort_out(x2)
PERM_IN(x1, x2)  =  PERM_IN(x1)
U51(x1, x2, x3, x4, x5)  =  U51(x5)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

PERM_IN(.(X, .(Y, [])), .(U, .(V, []))) → U51(X, Y, U, V, delete_in(U, .(X, Y), Z))
U51(X, Y, U, V, delete_out(U, .(X, Y), Z)) → PERM_IN(Z, V)

The TRS R consists of the following rules:

delete_in(X, .(Y, Z), W) → U7(X, Y, Z, W, delete_in(X, Z, W))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U7(X, Y, Z, W, delete_out(X, Z, W)) → delete_out(X, .(Y, Z), W)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delete_in(x1, x2, x3)  =  delete_in(x2)
U7(x1, x2, x3, x4, x5)  =  U7(x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
PERM_IN(x1, x2)  =  PERM_IN(x1)
U51(x1, x2, x3, x4, x5)  =  U51(x5)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ UsableRulesReductionPairsProof

Q DP problem:
The TRS P consists of the following rules:

U51(delete_out(U, Z)) → PERM_IN(Z)
PERM_IN(.(X, .(Y, []))) → U51(delete_in(.(X, Y)))

The TRS R consists of the following rules:

delete_in(.(Y, Z)) → U7(delete_in(Z))
delete_in(.(X, Y)) → delete_out(X, Y)
U7(delete_out(X, W)) → delete_out(X, W)

The set Q consists of the following terms:

delete_in(x0)
U7(x0)

We have to consider all (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

U51(delete_out(U, Z)) → PERM_IN(Z)
PERM_IN(.(X, .(Y, []))) → U51(delete_in(.(X, Y)))
The following rules are removed from R:

U7(delete_out(X, W)) → delete_out(X, W)
Used ordering: POLO with Polynomial interpretation [25]:

POL(.(x1, x2)) = 1 + 2·x1 + x2   
POL(PERM_IN(x1)) = x1   
POL(U51(x1)) = x1   
POL(U7(x1)) = 1 + x1   
POL([]) = 1   
POL(delete_in(x1)) = x1   
POL(delete_out(x1, x2)) = 1 + x1 + x2   



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ UsableRulesReductionPairsProof
                          ↳ QDP
                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

delete_in(.(Y, Z)) → U7(delete_in(Z))
delete_in(.(X, Y)) → delete_out(X, Y)

The set Q consists of the following terms:

delete_in(x0)
U7(x0)

We have to consider all (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.